Nuprl Lemma : qless_transitivity
11,40
postcript
pdf
a
,
b
,
c
:
.
a
<
b
b
<
c
a
<
c
latex
Definitions
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
Lemmas
qless
trans
qorder
origin
a, b, c:
. a < b 
b < c a < c a, b, c:. a < b b < c a < c x:A. B(x)
B(x)